(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_UFBV)
(declare-fun f0 ( (_ BitVec 3)) (_ BitVec 4))
(declare-fun f1 ( (_ BitVec 14) (_ BitVec 4)) (_ BitVec 12))
(declare-fun p0 ( (_ BitVec 15)) Bool)
(declare-fun p1 ( (_ BitVec 13) (_ BitVec 3)) Bool)
(declare-fun v0 () (_ BitVec 1))
(declare-fun v1 () (_ BitVec 4))
(declare-fun v2 () (_ BitVec 14))
(assert (let ((e3(_ bv17815 15)))
(let ((e4(_ bv2657 12)))
(let ((e5 (bvnand v2 ((_ sign_extend 2) e4))))
(let ((e6 (bvsrem ((_ sign_extend 8) v1) e4)))
(let ((e7 (f0 ((_ extract 11 9) e3))))
(let ((e8 (ite (p1 ((_ extract 13 1) e3) ((_ extract 10 8) e3)) (_ bv1 1) (_ bv0 1))))
(let ((e9 (ite (p0 ((_ sign_extend 3) e4)) (_ bv1 1) (_ bv0 1))))
(let ((e10 (f1 ((_ extract 13 0) e3) e7)))
(let ((e11 (bvadd ((_ sign_extend 3) e9) v1)))
(let ((e12 (bvxor v1 e7)))
(let ((e13 (bvsub ((_ sign_extend 8) e12) e4)))
(let ((e14 ((_ repeat 1) e6)))
(let ((e15 (bvcomp ((_ sign_extend 2) e10) v2)))
(let ((e16 (bvnand v1 ((_ zero_extend 3) e8))))
(let ((e17 (bvlshr ((_ zero_extend 11) e15) e4)))
(let ((e18 (bvand v2 e5)))
(let ((e19 (bvneg e11)))
(let ((e20 (ite (bvule e18 ((_ zero_extend 2) e14)) (_ bv1 1) (_ bv0 1))))
(let ((e21 (bvsrem ((_ zero_extend 8) e11) e17)))
(let ((e22 (bvcomp ((_ zero_extend 2) e6) e18)))
(let ((e23 ((_ rotate_right 0) e12)))
(let ((e24 (ite (bvslt e11 e7) (_ bv1 1) (_ bv0 1))))
(let ((e25 (bvxor e23 e7)))
(let ((e26 (bvmul ((_ zero_extend 8) e11) e13)))
(let ((e27 ((_ extract 11 0) e3)))
(let ((e28 (bvsub e4 ((_ zero_extend 11) v0))))
(let ((e29 (bvuge e10 ((_ sign_extend 11) e8))))
(let ((e30 (bvsge e28 ((_ sign_extend 11) e9))))
(let ((e31 (bvult e19 v1)))
(let ((e32 (p0 ((_ zero_extend 3) e10))))
(let ((e33 (p1 ((_ zero_extend 1) e4) ((_ extract 3 1) e7))))
(let ((e34 (bvult e11 ((_ zero_extend 3) e15))))
(let ((e35 (= ((_ sign_extend 14) e8) e3)))
(let ((e36 (bvslt ((_ zero_extend 11) e9) e26)))
(let ((e37 (distinct e6 ((_ sign_extend 11) e9))))
(let ((e38 (bvule e21 e10)))
(let ((e39 (bvslt ((_ sign_extend 3) e26) e3)))
(let ((e40 (bvult e17 ((_ zero_extend 8) e25))))
(let ((e41 (bvugt ((_ sign_extend 3) e22) e12)))
(let ((e42 (distinct e23 ((_ zero_extend 3) e20))))
(let ((e43 (distinct ((_ sign_extend 8) e11) e26)))
(let ((e44 (bvsge ((_ sign_extend 8) e16) e26)))
(let ((e45 (bvsge ((_ sign_extend 11) e16) e3)))
(let ((e46 (bvule e10 e26)))
(let ((e47 (bvsge e13 e13)))
(let ((e48 (= ((_ zero_extend 11) e15) e13)))
(let ((e49 (bvule e20 v0)))
(let ((e50 (bvule e3 ((_ zero_extend 1) e5))))
(let ((e51 (bvsle e20 e15)))
(let ((e52 (= e19 ((_ sign_extend 3) e24))))
(let ((e53 (bvsle e21 ((_ zero_extend 8) e23))))
(let ((e54 (distinct e20 e24)))
(let ((e55 (bvugt e26 ((_ sign_extend 11) e9))))
(let ((e56 (bvuge v0 e22)))
(let ((e57 (bvult e27 e4)))
(let ((e58 (bvsle e13 ((_ sign_extend 8) e7))))
(let ((e59 (bvsge v2 e5)))
(let ((e60 (bvsle e17 ((_ sign_extend 11) e24))))
(let ((e61 (bvuge e5 ((_ sign_extend 2) e10))))
(let ((e62 (bvule e13 e17)))
(let ((e63 (bvsle ((_ sign_extend 2) e28) v2)))
(let ((e64 (bvuge ((_ sign_extend 10) e12) e5)))
(let ((e65 (bvslt e14 ((_ zero_extend 11) v0))))
(let ((e66 (bvsle e13 ((_ zero_extend 8) e7))))
(let ((e67 (distinct e26 ((_ zero_extend 8) e25))))
(let ((e68 (bvuge e18 ((_ sign_extend 13) e15))))
(let ((e69 (=> e34 e41)))
(let ((e70 (or e44 e40)))
(let ((e71 (not e43)))
(let ((e72 (not e45)))
(let ((e73 (or e36 e66)))
(let ((e74 (xor e60 e68)))
(let ((e75 (= e52 e56)))
(let ((e76 (not e47)))
(let ((e77 (=> e32 e61)))
(let ((e78 (or e39 e71)))
(let ((e79 (ite e75 e35 e72)))
(let ((e80 (not e64)))
(let ((e81 (and e33 e69)))
(let ((e82 (= e59 e30)))
(let ((e83 (not e82)))
(let ((e84 (or e49 e63)))
(let ((e85 (ite e51 e74 e46)))
(let ((e86 (=> e65 e70)))
(let ((e87 (and e67 e29)))
(let ((e88 (ite e73 e58 e48)))
(let ((e89 (ite e78 e54 e78)))
(let ((e90 (not e83)))
(let ((e91 (and e77 e62)))
(let ((e92 (xor e38 e81)))
(let ((e93 (or e79 e57)))
(let ((e94 (ite e80 e90 e42)))
(let ((e95 (and e85 e88)))
(let ((e96 (and e92 e93)))
(let ((e97 (= e50 e50)))
(let ((e98 (xor e97 e31)))
(let ((e99 (ite e86 e76 e96)))
(let ((e100 (=> e37 e95)))
(let ((e101 (xor e99 e99)))
(let ((e102 (not e98)))
(let ((e103 (ite e55 e91 e91)))
(let ((e104 (and e103 e87)))
(let ((e105 (= e53 e84)))
(let ((e106 (and e89 e89)))
(let ((e107 (ite e101 e102 e94)))
(let ((e108 (xor e105 e105)))
(let ((e109 (= e107 e106)))
(let ((e110 (or e109 e109)))
(let ((e111 (ite e100 e104 e108)))
(let ((e112 (and e110 e110)))
(let ((e113 (and e112 e112)))
(let ((e114 (and e111 e111)))
(let ((e115 (and e113 e114)))
e115
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
